| Definitions | Top, t  T, IdDeq, Id, Type,  x.A(x),  x:A. B(x),  x. t(x), f(x)?z, x:A  B(x), S  T, P   Q, False,  A, A B, State(ds), State(ds), , , Dsys, @i: only members of L read x, @i: k sends only links in L, @i: k affects only members of L, Prop, S  T, @i (with ds: ds action a:T precondition a(v) is P s v), P & Q, DeclaredType(ds;x), Knd, lnk-decl(l;dt), KindDeq, f  g, rcv(l,tg), Void, Valtype(da;k), type List, x:A B(x), x : v, source(l), @i: with declarations ds:dsda:da k(v) sends f s v on link l, @i: with declarations ds:dsda:daeffect of k(v) is x := f s v, @i: only L sends on (l with tg), @i: only L affects x : t, @i: x:T initially x = v, System, es realizer ind Rrframe compseq tag def, es realizer ind Rbframe compseq tag def, es realizer ind Raframe compseq tag def, es realizer ind Rpre compseq tag def, es realizer ind Rsends compseq tag def, es realizer ind Reffect compseq tag def, es realizer ind Rsframe compseq tag def, es realizer ind Rframe compseq tag def, es realizer ind Rinit compseq tag def, es realizer ind Rnone compseq tag def, [[R]],  b, R-Feasible(R), #$n, @loc: only members of L read x, @loc: k sends only on links in L, @loc: k writes only members of L, @loc precondition for a(v:T):P State(ds) v, sends knd(v:T) on l:tagged(g,State(ds),v):dt, @loc effect knd(v:T) x := f State(ds) v , only events in L send on lnk with tag, @loc only events in L change x:T, @loc x initially v:T,   , {x:A| B(x) }, R-size(R), n+m, left right,  , es realizer ind Rplus compseq tag def, left+right, s = t, Unit, IdLnk, a:A fp B(a), rec(x.A(x)), Realizer, P  Q, P Q, b,  , a = b, if b t else f fi,  x:A. B(x), <a,b>, {T}, SQType(T), s ~ t, true, x dom(f), P  Q, Normal(T), xdom(f). v=f(x) P(x;v), Normal(ds), Atom$n, Case b of inl(x) s(x) ; inr(y) t(y), f(x), True, isrcv_rcv{isrcv_rcv_compseq_tag_def:ObjectId}(tg; l), lnk_rcv{lnk_rcv_compseq_tag_def:ObjectId}(tg; l), tag_rcv{tag_rcv_compseq_tag_def:ObjectId}(tg; l),  T, isrcv(k), lnk(k), destination(l), f(a), x(s), EqDecider(T), a = b, tag(k), |
| Lemmas | eq lnk wf, deq wf, ldst wf, true wf, lnk wf, squash wf, isrcv wf, assert-eq-lnk, Id sq, tagof wf, Knd sq, fpf-cap-single-join, bool cases, lnk-decl-cap, fpf-join-cap-sq, fpf-trivial-subtype-top, bool sq, btrue wf, fpf-cap-single1, fpf-dom wf, fpf-single-dom, fpf-cap-single, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, eq knd wf, bool wf, bnot wf, not wf, assert wf, assert-eq-knd, es realizer wf, unit wf, fpf wf, IdLnk wf, Rnone wf, Rplus wf, R-size wf, nat plus wf, Rinit wf, Rframe wf, Rsframe wf, Reffect wf, Rsends wf, Rpre wf, Raframe wf, Rbframe wf, R-Feasible wf, Rrframe wf, le wf, m-sys-null wf, d-single-init wf, d-single-frame wf, d-single-sframe wf, d-single-effect wf, d-single-sends wf, lsrc wf, ma-valtype wf, fpf-join wf, fpf-single wf, Knd wf, lnk-decl wf, Kind-deq wf, rcv wf, decl-type wf, d-single-pre wf, ma-state wf, decl-state wf, d-single-aframe wf, d-single-bframe wf, d-single-rframe wf, ma-empty wf, fpf-cap wf, Id wf, id-deq wf, top wf |